f(x, y) → g(x, y)
g(h(x), y) → h(f(x, y))
g(h(x), y) → h(g(x, y))
↳ QTRS
↳ DependencyPairsProof
f(x, y) → g(x, y)
g(h(x), y) → h(f(x, y))
g(h(x), y) → h(g(x, y))
F(x, y) → G(x, y)
G(h(x), y) → F(x, y)
G(h(x), y) → G(x, y)
f(x, y) → g(x, y)
g(h(x), y) → h(f(x, y))
g(h(x), y) → h(g(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F(x, y) → G(x, y)
G(h(x), y) → F(x, y)
G(h(x), y) → G(x, y)
f(x, y) → g(x, y)
g(h(x), y) → h(f(x, y))
g(h(x), y) → h(g(x, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(h(x), y) → F(x, y)
G(h(x), y) → G(x, y)
Used ordering: Polynomial interpretation [25,35]:
F(x, y) → G(x, y)
The value of delta used in the strict ordering is 45/16.
POL(h(x1)) = 9/4 + (13/4)x_1
POL(G(x1, x2)) = 1/4 + (5/4)x_1
POL(F(x1, x2)) = 1/4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
F(x, y) → G(x, y)
f(x, y) → g(x, y)
g(h(x), y) → h(f(x, y))
g(h(x), y) → h(g(x, y))